/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Yury Kudryashov, Kim Morrison
-/
module

public import Mathlib.Algebra.Module.Defs
public import Mathlib.Data.Finsupp.Basic
public import Mathlib.Data.Finsupp.SMulWithZero

/-!
# Monoid algebras

When the domain of a `Finsupp` has a multiplicative or additive structure, we can define
a convolution product. To mathematicians this structure is known as the "monoid algebra",
i.e. the finite formal linear combinations over a given semiring of elements of a monoid `M`.
The "group ring" `ℤ[G]` or the "group algebra" `k[G]` are typical uses.

In fact the construction of the "monoid algebra" makes sense when `M` is not even a monoid, but
merely a magma, i.e., when `M` carries a multiplication which is not required to satisfy any
conditions at all. In this case the construction yields a not-necessarily-unital,
not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such
algebras to magmas, and we prove this as `MonoidAlgebra.liftMagma`.

In this file we define `MonoidAlgebra R M := M →₀ R`, and `AddMonoidAlgebra R M`
in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:
```
Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)
```
Note: `Polynomial R` is currently a wrapper around `AddMonoidAlgebra R ℕ` and not defeq to it.
There is ongoing work to make it defeq.
See https://github.com/leanprover-community/mathlib4/pull/25273

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

## Notation

We introduce the notation `R[M]` for both `MonoidAlgebra R M` and `AddMonoidAlgebra R M`.
The notations are scoped to their respective namespaces, and which one `R[M]` resolves to therefore
depends on which of the two namespaces is open.
-/

@[expose] public section

assert_not_exists NonUnitalAlgHom AlgEquiv

noncomputable section

open Finsupp hiding single

-- We make sure the additivisable argument comes first to avoid doing
-- `to_additive (relevant_arg := 2)` everywhere.
variable {G M N O ι R S : Type*}

/-- The monoid algebra over a semiring `R` generated by the monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product. -/
@[to_additive (relevant_arg := 2)
/-- The additive monoid algebra over a semiring `R` generated by the additive monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product. -/, to_additive_dont_translate]
def MonoidAlgebra (R M : Type*) [Semiring R] : Type _ := M →₀ R

namespace AddMonoidAlgebra

@[inherit_doc AddMonoidAlgebra]
scoped syntax:max (priority := high) term noWs "[" term "]" : term

macro_rules | `($R[$M]) => `(AddMonoidAlgebra $R $M)

/-- Unexpander for `AddMonoidAlgebra`. -/
@[scoped app_unexpander AddMonoidAlgebra]
meta def unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $R $M) => `($R[$M])
  | _ => throw ()

end AddMonoidAlgebra

namespace MonoidAlgebra

@[inherit_doc MonoidAlgebra]
scoped syntax:max (priority := high) term noWs "[" term "]" : term

macro_rules | `($R[$M]) => `(MonoidAlgebra $R $M)

/-- Unexpander for `MonoidAlgebra`. -/
@[scoped app_unexpander MonoidAlgebra]
meta def unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $R $M) => `($R[$M])
  | _ => throw ()

section Semiring
variable [Semiring R] {x y : R[M]} {r r₁ r₂ : R} {m m' m₁ m₂ : M}

@[to_additive] instance inhabited : Inhabited R[M] :=
  inferInstanceAs <| Inhabited <| M →₀ R

@[to_additive] instance nontrivial [Nontrivial R] [Nonempty M] : Nontrivial R[M] :=
  inferInstanceAs <| Nontrivial <| M →₀ R

@[to_additive] instance unique [Subsingleton R] : Unique R[M] :=
  inferInstanceAs <| Unique <| M →₀ R

@[to_additive] instance addCommMonoid : AddCommMonoid R[M] :=
  inferInstanceAs <| AddCommMonoid <| M →₀ R

@[to_additive] instance instIsCancelAdd [IsCancelAdd R] : IsCancelAdd R[M] :=
  inferInstanceAs <| IsCancelAdd <| M →₀ R

@[to_additive] instance instCoeFun : CoeFun R[M] fun _ ↦ M → R :=
  inferInstanceAs <| CoeFun (M →₀ R) fun _ ↦ M → R

/-- A copy of `Finsupp.ext` for `MonoidAlgebra`. -/
@[to_additive (attr := ext) /-- A copy of `Finsupp.ext` for `AddMonoidAlgebra`. -/]
lemma ext ⦃f g : R[M]⦄ (hfg : ∀ m, f m = g m) : f = g := Finsupp.ext hfg

-- TODO: This definition is very leaky, and we later have frequent problems conflating the two
-- versions of `single`. Perhaps someone wants to try making this a `def` rather than an `abbrev`?
-- In Mathlib 3 this was locally reducible.
/-- `MonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : R[M]`. -/
@[to_additive
/-- `AddMonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : R[M]`. -/]
abbrev single (m : M) (r : R) : R[M] := Finsupp.single m r

section SMul

/-! ### Basic scalar multiplication instances

This section collects instances needed for the algebraic structure of `Polynomial`,
which is defined in terms of `MonoidAlgebra`.
Further results on scalar multiplication can be found in
`Mathlib/Algebra/MonoidAlgebra/Module.lean`.
-/

variable {A : Type*} [SMulZeroClass A R]

@[to_additive (dont_translate := A) smulZeroClass]
instance smulZeroClass : SMulZeroClass A R[M] :=
  Finsupp.smulZeroClass

@[to_additive (attr := simp) (dont_translate := A) coeff_smul]
lemma smul_apply (a : A) (x : R[M]) (m : M) : (a • x) m = a • x m := rfl

@[to_additive (attr := simp) (dont_translate := A) smul_single]
lemma smul_single (a : A) (m : M) (r : R) : a • single m r = single m (a • r) := by
  ext; simp [single, ← Finsupp.smul_single]

@[to_additive (dont_translate := R) smul_single']
lemma smul_single' (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r) := smul_single ..

@[to_additive (dont_translate := N) distribSMul]
instance distribSMul [DistribSMul N R] : DistribSMul N R[M] :=
  Finsupp.distribSMul _ _

@[to_additive (dont_translate := N) isScalarTower]
instance isScalarTower [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] :
    IsScalarTower N O R[M] :=
  Finsupp.isScalarTower ..

@[to_additive (dont_translate := N) smulCommClass]
instance smulCommClass [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] :
    SMulCommClass N O R[M] :=
  Finsupp.smulCommClass ..

@[to_additive (dont_translate := N) isCentralScalar]
instance isCentralScalar [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] :
    IsCentralScalar N R[M] :=
  Finsupp.isCentralScalar ..

end SMul

@[to_additive (attr := simp, norm_cast)]
lemma coe_add (f g : R[G]) : ⇑(f + g) = f + g := rfl

@[to_additive]
lemma single_zero (m : M) : (single m 0 : R[M]) = 0 := by simp [single]

@[to_additive]
lemma single_add (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂ := by
  simp [single]

/-- `MonoidAlgebra.single` as an `AddMonoidHom`.

TODO: Rename to `singleAddMonoidHom`. -/
@[to_additive (attr := simps)
/-- `AddMonoidAlgebra.single` as an `AddMonoidHom`.

TODO: Rename to `singleAddMonoidHom`. -/]
def singleAddHom (m : M) : R →+ R[M] where
  toFun := single m
  map_zero' := single_zero _
  map_add' := single_add _

/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`,
then they are equal.

We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`.

TODO: Rename to `addMonoidHom_ext'`. -/
@[to_additive (attr := ext high)
/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`, then they are equal.

We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`.

TODO: Rename to `addMonoidHom_ext'`. -/]
lemma addHom_ext' {N : Type*} [AddZeroClass N] ⦃f g : R[M] →+ N⦄
    (hfg : ∀ m, f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g :=
  Finsupp.addHom_ext' hfg

@[to_additive]
lemma sum_single_index [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) :
    (single m r).sum h = h m r := by
  simp [h_zero]

@[to_additive (attr := simp)]
lemma sum_single (x : R[M]) : x.sum single = x := Finsupp.sum_single _

@[to_additive]
theorem single_apply {a a' : M} {b : R} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

@[to_additive (attr := simp)]
lemma single_eq_zero : single m r = 0 ↔ r = 0 := Finsupp.single_eq_zero

@[to_additive] lemma single_ne_zero : single m r ≠ 0 ↔ r ≠ 0 := by simp [single]

@[to_additive (attr := elab_as_elim)]
lemma induction_linear {p : R[M] → Prop} (x : R[M]) (zero : p 0)
    (add : ∀ x y : R[M], p x → p y → p (x + y)) (single : ∀ m r, p (single m r)) :
    p x :=
  Finsupp.induction_linear x zero (fun _ _ ↦ add _ _) (fun _ _ ↦ single _ _)

section One
variable [One M]

/-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere. -/
@[to_additive (dont_translate := R)
/-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere. -/]
instance one : One R[M] where one := single 1 1

@[to_additive (dont_translate := R) one_def]
lemma one_def : (1 : R[M]) = single 1 1 := rfl

end One

section Mul
variable [Mul M]

/-- The multiplication in a monoid algebra.

We make it irreducible so that Lean doesn't unfold it when trying to unify two different things. -/
@[irreducible] def mul' (x y : R[M]) : R[M] :=
  x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂)

/-- The product of `f g : k[G]` is the finitely supported function
whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
such that `x + y = a`. (Think of the product of multivariate
polynomials where `α` is the additive monoid of monomial exponents.) -/
instance _root_.AddMonoidAlgebra.instMul [Add M] : Mul (AddMonoidAlgebra R M) where
  mul f g := MonoidAlgebra.mul' (M := Multiplicative M) f g

/-- The product of `x y : R[M]` is the finitely supported function whose value at `m`
is the sum of `x m₁ * y m₂` over all pairs `m₁, m₂` such that `m₁ * m₂ = m`.

(Think of the group ring of a group.) -/
@[to_additive existing instMul]
instance instMul : Mul R[M] where mul := mul'

@[to_additive (dont_translate := R) mul_def]
lemma mul_def (x y : R[M]) :
    x * y = x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂) := by
  with_unfolding_all rfl

@[to_additive (dont_translate := R)]
instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring R[M] where
  zero_mul := by simp [mul_def]
  mul_zero := by simp [mul_def]
  -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
  left_distrib f g h := by
    classical
    simp only [mul_def]
    refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
      simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
  right_distrib f g h := by
    classical
    simp only [mul_def]
    refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
      simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

@[to_additive (dont_translate := R) mul_apply]
lemma mul_apply [DecidableEq M] (x y : R[M]) (m : M) :
    (x * y) m = x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 := by
  -- Porting note: `reducible` cannot be `local` so proof gets long.
  rw [mul_def, Finsupp.sum_apply]; congr; ext
  rw [Finsupp.sum_apply]; congr; ext
  apply single_apply

open Finset in
@[to_additive (dont_translate := R) mul_apply_antidiagonal]
lemma mul_apply_antidiagonal (x y : R[M]) (m : M) (s : Finset (M × M))
    (hs : ∀ {p}, p ∈ s ↔ p.1 * p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2 := by
  classical
  let F (p : M × M) : R := if p.1 * p.2 = m then x p.1 * y p.2 else 0
  calc
    (x * y) m = ∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂) := mul_apply ..
    _ = ∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m, x p.1 * y p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support, x p.1 * y p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x p.1 * y p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]

@[to_additive (attr := simp) (dont_translate := R) single_mul_single]
lemma single_mul_single (m₁ m₂ : M) (r₁ r₂ : R) :
    single m₁ r₁ * single m₂ r₂ = single (m₁ * m₂) (r₁ * r₂) := by simp [mul_def]

@[to_additive (attr := simp) (dont_translate := R) single_commute_single]
lemma single_commute_single (hm : Commute m₁ m₂) (hr : Commute r₁ r₂) :
    Commute (single m₁ r₁) (single m₂ r₂) := by simp [Commute, SemiconjBy, hm.eq, hr.eq]

@[to_additive (attr := simp) (dont_translate := R) single_commute]
lemma single_commute (hm : ∀ m', Commute m m') (hr : ∀ r', Commute r r') (x : R[M]) :
    Commute (single m r) x := by
  have : AddMonoidHom.mulLeft (single m r) = AddMonoidHom.mulRight (single m r) := by
    ext m' r' : 2; exact single_commute_single (hm m') (hr r')
  exact congr($this x)

@[to_additive (dont_translate := R) mul_single_apply_aux]
lemma mul_single_apply_aux (H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂) :
    (x * single m r) m₁ = x m₂ * r := by
  classical
  calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]

@[to_additive (dont_translate := R) single_mul_apply_aux]
lemma single_mul_apply_aux (H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂) :
    (single m r * x) m₁ = r * x m₂ := by
  classical
  calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]

@[to_additive (attr := simp) (dont_translate := R) mul_single_apply_of_not_exists_add]
lemma mul_single_apply_of_not_exists_mul (r : R) (x : R[M]) (h : ¬ ∃ d, m' = d * m) :
    (x * single m r) m' = 0 := by classical simp_all [mul_apply, eq_comm]

@[to_additive (attr := simp) (dont_translate := R) single_mul_apply_of_not_exists_add]
lemma single_mul_apply_of_not_exists_mul (r : R) (x : R[M]) (h : ¬ ∃ d, m' = m * d) :
    (single m r * x) m' = 0 := by classical simp_all [mul_apply, eq_comm]

variable (R M : Type*) [Semiring R] [Mul M] in
/-- The embedding of a magma into its magma algebra. -/
@[simps]
def ofMagma : M →ₙ* R[M] where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]

end Mul

section Semigroup
variable [Semigroup M]

@[to_additive (dont_translate := R)]
instance nonUnitalSemiring : NonUnitalSemiring R[M] where
  mul_assoc f g h := by
    -- Porting note: `reducible` cannot be `local` so proof gets long.
    simp only [mul_def]
    rw [sum_sum_index] <;> congr; on_goal 1 => ext a₁ b₁
    rw [sum_sum_index, sum_sum_index] <;> congr; on_goal 1 => ext a₂ b₂
    rw [sum_sum_index, sum_single_index] <;> congr; on_goal 1 => ext a₃ b₃
    on_goal 1 => rw [sum_single_index, mul_assoc, mul_assoc]
    all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
      mul_add, zero_mul, mul_zero, sum_zero, sum_add]

end Semigroup

section MulOneClass
variable [MulOneClass M]

@[to_additive (dont_translate := R)]
instance nonAssocSemiring : NonAssocSemiring R[M] where
  natCast n := single 1 n
  natCast_zero := by simp
  natCast_succ := by simp [one_def]
  one_mul := by simp [mul_def, one_def]
  mul_one := by simp [mul_def, one_def]

@[to_additive (dont_translate := R)]
lemma natCast_def (n : ℕ) : (n : R[M]) = single (1 : M) (n : R) := rfl

@[to_additive (dont_translate := R) mul_single_zero_apply]
lemma mul_single_one_apply (x : R[M]) (r : R) (m : M) : (x * single 1 r : R[M]) m = x m * r :=
  x.mul_single_apply_aux (by simp)

@[to_additive (dont_translate := R) single_zero_mul_apply]
lemma single_one_mul_apply (x : R[M]) (r : R) (m : M) : (single 1 r * x : R[M]) m = r * x m :=
  x.single_mul_apply_aux (by simp)

variable (R M : Type*) [Semiring R] [MulOneClass M] in
/-- The embedding of a unital magma into its magma algebra. -/
@[simps]
def of : M →* R[M] where
  __ := ofMagma R M
  toFun m := single m 1
  map_one' := rfl

lemma of_injective [Nontrivial R] : Function.Injective (of R M) := fun a b h ↦ by
  simpa using (single_eq_single_iff _ _ _ _).mp h

lemma of_commute (h : ∀ m', Commute m m') (f : R[M]) : Commute (of R M m) f :=
  single_commute h .one_left f

/-- `MonoidAlgebra.single` as a `MonoidHom` from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`MonoidAlgebra.single`. -/
@[simps]
def singleHom : R × M →* R[M] where
  toFun a := single a.2 a.1
  map_one' := rfl
  map_mul' _a _b := by simp

/-- `MonoidAlgebra.single 1` as a `RingHom` -/
@[to_additive (attr := simps) (dont_translate := R)
/-- `AddMonoidAlgebra.single 1` as a `RingHom` -/]
def singleOneRingHom : R →+* R[M] :=
  { singleAddHom 1 with
    toFun := single 1
    map_one' := rfl
    map_mul' := fun x y => by simp }

/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1` and
`single 1 r`, then they are equal. -/
@[to_additive (dont_translate := R S)
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1` and `single 0 r`,
then they are equal. -/]
lemma ringHom_ext [Semiring S] {f g : R[M] →+* S}
    (h₁ : ∀ r, f (single 1 r) = g (single 1 r)) (h_of : ∀ m, f (single m 1) = g (single m 1)) :
    f = g :=
  RingHom.coe_addMonoidHom_injective <| addHom_ext fun m r ↦ by
    simpa [← map_mul] using congr($(h₁ r) * $(h_of m))

/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1`
and `single 1 r`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
lemma ringHom_ext' [Semiring S] {f g : R[M] →+* S}
    (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
    (h_of : (f : R[M] →* S).comp (of R M) =
      (g : R[M] →* S).comp (of R M)) : f = g :=
  ringHom_ext (by simpa [DFunLike.ext_iff] using h₁) (by simpa [DFunLike.ext_iff] using h_of)

end MulOneClass

section Monoid
variable [Monoid M]

@[to_additive]
instance semiring : Semiring R[M] where

@[to_additive (attr := simp) (dont_translate := R) single_pow]
lemma single_pow (m : M) (r : R) : ∀ n : ℕ, single m r ^ n = single (m ^ n) (r ^ n)
  | 0 => by simp [one_def]
  | n + 1 => by simp [pow_succ, single_pow _ _ n]

lemma induction_on {p : R[M] → Prop} (x : R[M])
    (hM : ∀ m, p (of R M m)) (hadd : ∀ x y : R[M], p x → p y → p (x + y))
    (hsmul : ∀ (r : R) (x), p x → p (r • x)) : p x :=
  Finsupp.induction_linear x (by simpa using hsmul 0 (of R M 1) (hM 1))
    (fun x y hf hg => hadd x y hf hg) fun m r ↦ by simpa using hsmul r (of R M m) (hM m)

@[to_additive (dont_translate := R)]
instance isLocalHom_singleOneRingHom : IsLocalHom (singleOneRingHom (R := R) (M := M)) where
  map_nonunit x hx := by
    obtain ⟨⟨x, xi, hx, hxi⟩, rfl⟩ := hx
    simp_rw [MonoidAlgebra.ext_iff, singleOneRingHom_apply] at hx hxi ⊢
    specialize hx 1
    specialize hxi 1
    classical
    simp_rw [single_one_mul_apply, one_def, single_apply, if_pos] at hx
    simp_rw [mul_single_one_apply, one_def, single_apply, if_pos] at hxi
    exact ⟨⟨x, xi 1, hx, hxi⟩, rfl⟩

end Monoid

section Group
variable [Group G]

@[to_additive (attr := simp) (dont_translate := R) mul_single_apply]
lemma mul_single_apply (x : R[G]) (r : R) (g h : G) : (x * single g r) h = x (h * g⁻¹) * r :=
  mul_single_apply_aux <| by simp [eq_mul_inv_iff_mul_eq]

@[to_additive (attr := simp) (dont_translate := R) single_mul_apply]
lemma single_mul_apply (x : R[G]) (r : R) (g h : G) : (single g r * x) h = r * x (g⁻¹ * h) :=
  single_mul_apply_aux <| by simp [eq_inv_mul_iff_mul_eq]

@[to_additive (dont_translate := R) mul_apply_left]
lemma mul_apply_left (x y : R[G]) (g : G) : (x * y) g = x.sum fun h r ↦ r * y (h⁻¹ * g) := by
  classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]

@[to_additive (dont_translate := R) mul_apply_right]
lemma mul_apply_right (x y : R[G]) (g : G) : (x * y) g = y.sum fun h r ↦ x (g * h⁻¹) * r := by
  classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]

end Group
end Semiring

section CommSemiring
variable [CommSemiring R]

@[to_additive (dont_translate := R)]
instance nonUnitalCommSemiring [CommSemigroup M] : NonUnitalCommSemiring R[M] where
  mul_comm f g := by simp [mul_def, Finsupp.sum, mul_comm, f.support.sum_comm]

@[to_additive (dont_translate := R)]
lemma single_one_comm [MulOneClass M] (r : R) (f : R[M]) :
    single (1 : M) r * f = f * single (1 : M) r :=
  single_commute .one_left (.all _) f

section CommMonoid
variable [CommMonoid M]

@[to_additive (dont_translate := R)]
instance commSemiring : CommSemiring R[M] where

open Finset in
@[to_additive (dont_translate := R) prod_single]
lemma prod_single (s : Finset ι) (m : ι → M) (r : ι → R) :
    ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i) :=
  Finset.cons_induction_on s rfl fun i s hi ih ↦ by
    rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]

end CommMonoid
end CommSemiring

section Ring
variable [Ring R]

@[to_additive (dont_translate := R)]
instance addCommGroup : AddCommGroup R[M] :=
  inferInstanceAs <| AddCommGroup <| M →₀ R

@[to_additive (attr := simp) (dont_translate := R)]
lemma neg_apply (m : M) (x : R[M]) : (-x) m = -x m := rfl

@[to_additive (dont_translate := R)]
lemma single_neg (m : M) (r : R) : single m (-r) = -single m r := by simp [single]

@[to_additive (dont_translate := R)]
instance nonUnitalNonAssocRing [Mul M] : NonUnitalNonAssocRing R[M] where

@[to_additive (dont_translate := R)]
instance nonUnitalRing [Semigroup M] : NonUnitalRing R[M] where

@[to_additive (dont_translate := R)]
instance nonAssocRing [MulOneClass M] : NonAssocRing R[M] where
  intCast z := single 1 z
  intCast_ofNat n := by simp [natCast_def]
  intCast_negSucc n := by simp [natCast_def, one_def]

@[to_additive (dont_translate := R)]
lemma intCast_def [MulOneClass M] (z : ℤ) : (z : R[M]) = single 1 (z : R) := rfl

@[to_additive (dont_translate := R)]
instance ring [Monoid M] : Ring R[M] where

end Ring

section CommRing
variable [CommRing R]

@[to_additive (dont_translate := R)]
instance nonUnitalCommRing [CommSemigroup M] : NonUnitalCommRing R[M] where

@[to_additive (dont_translate := R)]
instance commRing [CommMonoid M] : CommRing R[M] where

end CommRing
end MonoidAlgebra

/-! ### Additive monoids -/

namespace AddMonoidAlgebra
variable [Semiring R]

section

variable (R M : Type*) [Semiring R]

/-- The embedding of an additive magma into its additive magma algebra. -/
@[simps]
def ofMagma [Add M] : Multiplicative M →ₙ* R[M] where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]; rfl

/-- Embedding of a magma with zero into its magma algebra. -/
def of [AddZeroClass M] : Multiplicative M →* R[M] :=
  { ofMagma R M with
    toFun := fun a => single a 1
    map_one' := rfl }

/-- Embedding of a magma with zero `M`, into its magma algebra, having `M` as source. -/
def of' : M → R[M] := fun m => single m 1

end

@[simp]
theorem of_apply [AddZeroClass M] (a : Multiplicative M) : of R M a = single a.toAdd 1 :=
  rfl

@[simp]
theorem of'_apply (a : M) : of' R M a = single a 1 :=
  rfl

theorem of'_eq_of [AddZeroClass M] (a : M) : of' R M a = of R M (.ofAdd a) := rfl

theorem of_injective [Nontrivial R] [AddZeroClass M] : Function.Injective (of R M) :=
  MonoidAlgebra.of_injective

lemma of'_commute [AddZeroClass M] {a : M} (h : ∀ a', AddCommute a a') (f : AddMonoidAlgebra R M) :
    Commute (of' R M a) f :=
  single_commute h .one_left f

/-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [AddZeroClass M] : R × Multiplicative M →* R[M] where
  toFun a := single a.2.toAdd a.1
  map_one' := rfl
  map_mul' _a _b := (single_mul_single ..).symm

theorem induction_on [AddMonoid M] {p : R[M] → Prop} (x : R[M])
    (hM : ∀ m, p (of R M <| .ofAdd m)) (hadd : ∀ x y : R[M], p x → p y → p (x + y))
    (hsmul : ∀ (r : R) (x), p x → p (r • x)) : p x :=
  Finsupp.induction_linear x (by simpa using hsmul 0 (of R M 1) (hM 0))
    (fun x y hf hg ↦ hadd x y hf hg) fun m r ↦ by simpa using hsmul r (of R M m) (hM m)

/-! #### Algebra structure -/

/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1`
and `single 0 r`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' [Semiring S] [AddMonoid M] {f g : R[M] →+* S}
    (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
    (h_of : (f : R[M] →* S).comp (of R M) = (g : R[M] →* S).comp (of R M)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

end AddMonoidAlgebra
